/**
 * Copyright (c) 2011 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.test.jmlsyp.parsing;

import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;

import edu.cmu.cs.crystal.annotations.FailingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * @author kevin
 * @since Jan 30, 2011
 */
@FailingTest(1) // 1 failure to test making an assumption that's not already known
@UseAnalyses("SymbolicChecker")
public class Parsing {
	
	//@ invariant 0 <= i;
	private int i;
	
	/*@ ensures \result == a + b; */
	public int add(int a, int b) {
		return a + b;
	}

	//@ ensures \result == a - b;
	public int sub(int a, int b) {
		return a - b;
	}
	
	/*@ requires a != 0.0 | b != 0.0;
	  @ ensures \result == a / b; 
	 */
	public double div(double a, double b) {
		return a / b;
	}
	
	/**
	 * test {@code \old} in post-condition of called method
	 * and in method's own post-condition
	 * @return old {@link #i}
	 */
	//@ ensures \result == \old(i);
	@Excl public int inc() {
		int result;
		imm: result = i;
		voidInc();
		return result;
	}
	
	/**
	 * test default return post-condition checking with {@code \old}
	 */
	//@ ensures i == \old(i) + 1;
	@Excl(mod = "i") public void voidInc() {
		excl: i++;
	}
	
	/**
	 * simple test client for method with post-condition
	 */
	public void testSub() {
		int three = sub(5, 2);
		//@ assert three == 3;
	}
	
	/**
	 * use {@code assume} and {@code assert} in client for method with
	 * {@link \old} in post-condition
	 */
	@Excl public void testInc() {
		//@ assume i == 0; // fail: know nothing about i
		int o = inc();
		//@ assert o == 0;
	}
	
	/**
	 * test simple loop invariant for {@code while} loop
	 * @param start
	 */
	//@ requires 0 <= start;
	public void whileInv(int start) {
		//@ loop_invariant 0 <= start;
		//@ decreasing start; 
		while (0 < start) {
			--start;
		}
	}

	/**
	 * test fancy loop invariant for {@code for} loop
	 * @param start
	 */
	public void forInv(int start) {
		// TODO maintaining start == \old(start) + i;
		//@ decreases 10-i;
		for (int i = 0; i < 10; ++i) {
			++start;
		}
	}
	
	/** test that class invariant is provable */
	@Imm public void classInv() {
		imm: { //@ assert 0 <= i; 
		}
	}
	
	/** test \old in asserts rather than post-conditions */
	public void preInAssert(int x) {
		++x;
		//@ assert x == \pre(x) + 1;
		// \old works too but JML spec recommends to use \pre in asserts
		//@ assert \old(x) == x - 1;
	}
	
	/** test parsing \type expressions, which we support because it's easy */
	public void typeLiterals() {
		//@ assert \type(int) == int.class;
		//@ assert \type(Object[]) == Object[].class;
	}
}
